YES 0.651
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| ((dropWhile :: (a -> Bool) -> [a] -> [a]) :: (a -> Bool) -> [a] -> [a]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(vv : vw)
is replaced by the following term
vv : vw
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((dropWhile :: (a -> Bool) -> [a] -> [a]) :: (a -> Bool) -> [a] -> [a]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
dropWhile | p [] | = [] |
dropWhile | p (vv : vw) | |
is transformed to
dropWhile | p [] | = dropWhile3 p [] |
dropWhile | p (vv : vw) | = dropWhile2 p (vv : vw) |
dropWhile0 | p vv vw True | = vv : vw |
dropWhile1 | p vv vw True | = dropWhile p vw |
dropWhile1 | p vv vw False | = dropWhile0 p vv vw otherwise |
dropWhile2 | p (vv : vw) | = dropWhile1 p vv vw (p vv) |
dropWhile3 | p [] | = [] |
dropWhile3 | wv ww | = dropWhile2 wv ww |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (dropWhile :: (a -> Bool) -> [a] -> [a]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_dropWhile1(wx3, wx40, wx41, ba) → new_dropWhile(wx3, wx41, ba)
new_dropWhile(wx3, :(wx40, wx41), ba) → new_dropWhile1(wx3, wx40, wx41, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_dropWhile(wx3, :(wx40, wx41), ba) → new_dropWhile1(wx3, wx40, wx41, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 3 >= 4
- new_dropWhile1(wx3, wx40, wx41, ba) → new_dropWhile(wx3, wx41, ba)
The graph contains the following edges 1 >= 1, 3 >= 2, 4 >= 3